A, B:Type, f:(A(B + Top)), P:(A), p:(x:A. Dec(P(x))), x:A.
(can-apply(p-co-restrict(f;p);x))  (do-apply(p-co-restrict(f;p);x) = do-apply(f;x)  B) 

latex

ProofTree

Definitions	Type, , x:A. B(x), t  T, True, Void, x:A.B(x), Top, x:AB(x), S  T, left + right, suptype(S; T), P  Q, x. t(x), f(a), x(s), T, p-co-filter(f), do-apply(f;x), can-apply(f;x), , b, P  Q, x:A  B(x), P & Q, P  Q, s = t, Dec(P), x.A(x), f o g  , p-co-restrict(f;p)
Lemmas	p-compose wf, p-co-filter wf, decidable wf, do-apply-compose, can-apply-compose-iff, do-apply wf, assert wf, bool wf, can-apply wf, squash wf, true wf, top wf, do-apply-p-co-filter